Nuprl Lemma : length-map
0,22
postcript
pdf
f
:Top,
T
:Type,
L
:
T
List. ||map(
f
;
L
)|| ~ ||
L
||
latex
Definitions
Top
,
x
:
A
.
B
(
x
)
,
t
T
Lemmas
top
wf
origin
f:Top, T:Type, L:T List. ||map(f;L)|| ~ ||L|| f:Top, T:Type, L:T List. ||map(f;L)|| ~ ||L|| x:A. B(x)
T